The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

S is empty.
Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Types:
intersect'ii'in :: cons:nil → cons:nil → intersect'ii'out
cons :: if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil
intersect'ii'out :: intersect'ii'out
u'1'1 :: intersect'ii'out → intersect'ii'out
u'2'1 :: intersect'ii'out → intersect'ii'out
reduce'ii'in :: sequent → sequent → reduce'ii'out
sequent :: cons:nil → cons:nil → sequent
if :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'3'1 :: reduce'ii'out → reduce'ii'out
x'2b :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
x'2d :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
reduce'ii'out :: reduce'ii'out
iff :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'4'1 :: reduce'ii'out → reduce'ii'out
x'2a :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'5'1 :: reduce'ii'out → reduce'ii'out
u'6'1 :: reduce'ii'out → if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil → sequent → reduce'ii'out
u'6'2 :: reduce'ii'out → reduce'ii'out
u'7'1 :: reduce'ii'out → reduce'ii'out
u'8'1 :: reduce'ii'out → reduce'ii'out
u'9'1 :: reduce'ii'out → reduce'ii'out
p :: a → if:x'2d:x'2b:iff:x'2a:p
u'10'1 :: reduce'ii'out → reduce'ii'out
u'11'1 :: reduce'ii'out → reduce'ii'out
u'12'1 :: reduce'ii'out → cons:nil → if:x'2d:x'2b:iff:x'2a:p → cons:nil → sequent → reduce'ii'out
u'12'2 :: reduce'ii'out → reduce'ii'out
u'13'1 :: reduce'ii'out → reduce'ii'out
nil :: cons:nil
u'14'1 :: reduce'ii'out → reduce'ii'out
u'15'1 :: intersect'ii'out → reduce'ii'out
tautology'i'in :: if:x'2d:x'2b:iff:x'2a:p → tautology'i'out
u'16'1 :: reduce'ii'out → tautology'i'out
tautology'i'out :: tautology'i'out
hole_intersect'ii'out1_3 :: intersect'ii'out
hole_cons:nil2_3 :: cons:nil
hole_if:x'2d:x'2b:iff:x'2a:p3_3 :: if:x'2d:x'2b:iff:x'2a:p
hole_reduce'ii'out4_3 :: reduce'ii'out
hole_sequent5_3 :: sequent
hole_a6_3 :: a
hole_tautology'i'out7_3 :: tautology'i'out
gen_cons:nil8_3 :: Nat → cons:nil
gen_if:x'2d:x'2b:iff:x'2a:p9_3 :: Nat → if:x'2d:x'2b:iff:x'2a:p

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
intersect'ii'in, reduce'ii'in

They will be analysed ascendingly in the following order:
intersect'ii'in < reduce'ii'in

(6) Obligation:

Innermost TRS:
Rules:
intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Types:
intersect'ii'in :: cons:nil → cons:nil → intersect'ii'out
cons :: if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil
intersect'ii'out :: intersect'ii'out
u'1'1 :: intersect'ii'out → intersect'ii'out
u'2'1 :: intersect'ii'out → intersect'ii'out
reduce'ii'in :: sequent → sequent → reduce'ii'out
sequent :: cons:nil → cons:nil → sequent
if :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'3'1 :: reduce'ii'out → reduce'ii'out
x'2b :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
x'2d :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
reduce'ii'out :: reduce'ii'out
iff :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'4'1 :: reduce'ii'out → reduce'ii'out
x'2a :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'5'1 :: reduce'ii'out → reduce'ii'out
u'6'1 :: reduce'ii'out → if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil → sequent → reduce'ii'out
u'6'2 :: reduce'ii'out → reduce'ii'out
u'7'1 :: reduce'ii'out → reduce'ii'out
u'8'1 :: reduce'ii'out → reduce'ii'out
u'9'1 :: reduce'ii'out → reduce'ii'out
p :: a → if:x'2d:x'2b:iff:x'2a:p
u'10'1 :: reduce'ii'out → reduce'ii'out
u'11'1 :: reduce'ii'out → reduce'ii'out
u'12'1 :: reduce'ii'out → cons:nil → if:x'2d:x'2b:iff:x'2a:p → cons:nil → sequent → reduce'ii'out
u'12'2 :: reduce'ii'out → reduce'ii'out
u'13'1 :: reduce'ii'out → reduce'ii'out
nil :: cons:nil
u'14'1 :: reduce'ii'out → reduce'ii'out
u'15'1 :: intersect'ii'out → reduce'ii'out
tautology'i'in :: if:x'2d:x'2b:iff:x'2a:p → tautology'i'out
u'16'1 :: reduce'ii'out → tautology'i'out
tautology'i'out :: tautology'i'out
hole_intersect'ii'out1_3 :: intersect'ii'out
hole_cons:nil2_3 :: cons:nil
hole_if:x'2d:x'2b:iff:x'2a:p3_3 :: if:x'2d:x'2b:iff:x'2a:p
hole_reduce'ii'out4_3 :: reduce'ii'out
hole_sequent5_3 :: sequent
hole_a6_3 :: a
hole_tautology'i'out7_3 :: tautology'i'out
gen_cons:nil8_3 :: Nat → cons:nil
gen_if:x'2d:x'2b:iff:x'2a:p9_3 :: Nat → if:x'2d:x'2b:iff:x'2a:p

Generator Equations:
gen_cons:nil8_3(0) ⇔ nil
gen_cons:nil8_3(+(x, 1)) ⇔ cons(p(hole_a6_3), gen_cons:nil8_3(x))
gen_if:x'2d:x'2b:iff:x'2a:p9_3(0) ⇔ p(hole_a6_3)
gen_if:x'2d:x'2b:iff:x'2a:p9_3(+(x, 1)) ⇔ if(p(hole_a6_3), gen_if:x'2d:x'2b:iff:x'2a:p9_3(x))

The following defined symbols remain to be analysed:
intersect'ii'in, reduce'ii'in

They will be analysed ascendingly in the following order:
intersect'ii'in < reduce'ii'in

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3))) → *10_3, rt ∈ Ω(n11₃)

Induction Base:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, 0)))

Induction Step:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, +(n11_3, 1)))) →_R^Ω(1)
u'1'1(intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3)))) →_IH
u'1'1(*10_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Types:
intersect'ii'in :: cons:nil → cons:nil → intersect'ii'out
cons :: if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil
intersect'ii'out :: intersect'ii'out
u'1'1 :: intersect'ii'out → intersect'ii'out
u'2'1 :: intersect'ii'out → intersect'ii'out
reduce'ii'in :: sequent → sequent → reduce'ii'out
sequent :: cons:nil → cons:nil → sequent
if :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'3'1 :: reduce'ii'out → reduce'ii'out
x'2b :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
x'2d :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
reduce'ii'out :: reduce'ii'out
iff :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'4'1 :: reduce'ii'out → reduce'ii'out
x'2a :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'5'1 :: reduce'ii'out → reduce'ii'out
u'6'1 :: reduce'ii'out → if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil → sequent → reduce'ii'out
u'6'2 :: reduce'ii'out → reduce'ii'out
u'7'1 :: reduce'ii'out → reduce'ii'out
u'8'1 :: reduce'ii'out → reduce'ii'out
u'9'1 :: reduce'ii'out → reduce'ii'out
p :: a → if:x'2d:x'2b:iff:x'2a:p
u'10'1 :: reduce'ii'out → reduce'ii'out
u'11'1 :: reduce'ii'out → reduce'ii'out
u'12'1 :: reduce'ii'out → cons:nil → if:x'2d:x'2b:iff:x'2a:p → cons:nil → sequent → reduce'ii'out
u'12'2 :: reduce'ii'out → reduce'ii'out
u'13'1 :: reduce'ii'out → reduce'ii'out
nil :: cons:nil
u'14'1 :: reduce'ii'out → reduce'ii'out
u'15'1 :: intersect'ii'out → reduce'ii'out
tautology'i'in :: if:x'2d:x'2b:iff:x'2a:p → tautology'i'out
u'16'1 :: reduce'ii'out → tautology'i'out
tautology'i'out :: tautology'i'out
hole_intersect'ii'out1_3 :: intersect'ii'out
hole_cons:nil2_3 :: cons:nil
hole_if:x'2d:x'2b:iff:x'2a:p3_3 :: if:x'2d:x'2b:iff:x'2a:p
hole_reduce'ii'out4_3 :: reduce'ii'out
hole_sequent5_3 :: sequent
hole_a6_3 :: a
hole_tautology'i'out7_3 :: tautology'i'out
gen_cons:nil8_3 :: Nat → cons:nil
gen_if:x'2d:x'2b:iff:x'2a:p9_3 :: Nat → if:x'2d:x'2b:iff:x'2a:p

Lemmas:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3))) → *10_3, rt ∈ Ω(n11₃)

Generator Equations:
gen_cons:nil8_3(0) ⇔ nil
gen_cons:nil8_3(+(x, 1)) ⇔ cons(p(hole_a6_3), gen_cons:nil8_3(x))
gen_if:x'2d:x'2b:iff:x'2a:p9_3(0) ⇔ p(hole_a6_3)
gen_if:x'2d:x'2b:iff:x'2a:p9_3(+(x, 1)) ⇔ if(p(hole_a6_3), gen_if:x'2d:x'2b:iff:x'2a:p9_3(x))

The following defined symbols remain to be analysed:
reduce'ii'in

(10) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol reduce'ii'in.

(11) Obligation:

Innermost TRS:
Rules:
intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Types:
intersect'ii'in :: cons:nil → cons:nil → intersect'ii'out
cons :: if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil
intersect'ii'out :: intersect'ii'out
u'1'1 :: intersect'ii'out → intersect'ii'out
u'2'1 :: intersect'ii'out → intersect'ii'out
reduce'ii'in :: sequent → sequent → reduce'ii'out
sequent :: cons:nil → cons:nil → sequent
if :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'3'1 :: reduce'ii'out → reduce'ii'out
x'2b :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
x'2d :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
reduce'ii'out :: reduce'ii'out
iff :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'4'1 :: reduce'ii'out → reduce'ii'out
x'2a :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'5'1 :: reduce'ii'out → reduce'ii'out
u'6'1 :: reduce'ii'out → if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil → sequent → reduce'ii'out
u'6'2 :: reduce'ii'out → reduce'ii'out
u'7'1 :: reduce'ii'out → reduce'ii'out
u'8'1 :: reduce'ii'out → reduce'ii'out
u'9'1 :: reduce'ii'out → reduce'ii'out
p :: a → if:x'2d:x'2b:iff:x'2a:p
u'10'1 :: reduce'ii'out → reduce'ii'out
u'11'1 :: reduce'ii'out → reduce'ii'out
u'12'1 :: reduce'ii'out → cons:nil → if:x'2d:x'2b:iff:x'2a:p → cons:nil → sequent → reduce'ii'out
u'12'2 :: reduce'ii'out → reduce'ii'out
u'13'1 :: reduce'ii'out → reduce'ii'out
nil :: cons:nil
u'14'1 :: reduce'ii'out → reduce'ii'out
u'15'1 :: intersect'ii'out → reduce'ii'out
tautology'i'in :: if:x'2d:x'2b:iff:x'2a:p → tautology'i'out
u'16'1 :: reduce'ii'out → tautology'i'out
tautology'i'out :: tautology'i'out
hole_intersect'ii'out1_3 :: intersect'ii'out
hole_cons:nil2_3 :: cons:nil
hole_if:x'2d:x'2b:iff:x'2a:p3_3 :: if:x'2d:x'2b:iff:x'2a:p
hole_reduce'ii'out4_3 :: reduce'ii'out
hole_sequent5_3 :: sequent
hole_a6_3 :: a
hole_tautology'i'out7_3 :: tautology'i'out
gen_cons:nil8_3 :: Nat → cons:nil
gen_if:x'2d:x'2b:iff:x'2a:p9_3 :: Nat → if:x'2d:x'2b:iff:x'2a:p

Lemmas:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3))) → *10_3, rt ∈ Ω(n11₃)

Generator Equations:
gen_cons:nil8_3(0) ⇔ nil
gen_cons:nil8_3(+(x, 1)) ⇔ cons(p(hole_a6_3), gen_cons:nil8_3(x))
gen_if:x'2d:x'2b:iff:x'2a:p9_3(0) ⇔ p(hole_a6_3)
gen_if:x'2d:x'2b:iff:x'2a:p9_3(+(x, 1)) ⇔ if(p(hole_a6_3), gen_if:x'2d:x'2b:iff:x'2a:p9_3(x))

No more defined symbols left to analyse.

(12) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3))) → *10_3, rt ∈ Ω(n11₃)

(13) BOUNDS(n^1, INF)

(14) Obligation:

Innermost TRS:
Rules:
intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Types:
intersect'ii'in :: cons:nil → cons:nil → intersect'ii'out
cons :: if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil
intersect'ii'out :: intersect'ii'out
u'1'1 :: intersect'ii'out → intersect'ii'out
u'2'1 :: intersect'ii'out → intersect'ii'out
reduce'ii'in :: sequent → sequent → reduce'ii'out
sequent :: cons:nil → cons:nil → sequent
if :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'3'1 :: reduce'ii'out → reduce'ii'out
x'2b :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
x'2d :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
reduce'ii'out :: reduce'ii'out
iff :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'4'1 :: reduce'ii'out → reduce'ii'out
x'2a :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'5'1 :: reduce'ii'out → reduce'ii'out
u'6'1 :: reduce'ii'out → if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil → sequent → reduce'ii'out
u'6'2 :: reduce'ii'out → reduce'ii'out
u'7'1 :: reduce'ii'out → reduce'ii'out
u'8'1 :: reduce'ii'out → reduce'ii'out
u'9'1 :: reduce'ii'out → reduce'ii'out
p :: a → if:x'2d:x'2b:iff:x'2a:p
u'10'1 :: reduce'ii'out → reduce'ii'out
u'11'1 :: reduce'ii'out → reduce'ii'out
u'12'1 :: reduce'ii'out → cons:nil → if:x'2d:x'2b:iff:x'2a:p → cons:nil → sequent → reduce'ii'out
u'12'2 :: reduce'ii'out → reduce'ii'out
u'13'1 :: reduce'ii'out → reduce'ii'out
nil :: cons:nil
u'14'1 :: reduce'ii'out → reduce'ii'out
u'15'1 :: intersect'ii'out → reduce'ii'out
tautology'i'in :: if:x'2d:x'2b:iff:x'2a:p → tautology'i'out
u'16'1 :: reduce'ii'out → tautology'i'out
tautology'i'out :: tautology'i'out
hole_intersect'ii'out1_3 :: intersect'ii'out
hole_cons:nil2_3 :: cons:nil
hole_if:x'2d:x'2b:iff:x'2a:p3_3 :: if:x'2d:x'2b:iff:x'2a:p
hole_reduce'ii'out4_3 :: reduce'ii'out
hole_sequent5_3 :: sequent
hole_a6_3 :: a
hole_tautology'i'out7_3 :: tautology'i'out
gen_cons:nil8_3 :: Nat → cons:nil
gen_if:x'2d:x'2b:iff:x'2a:p9_3 :: Nat → if:x'2d:x'2b:iff:x'2a:p

Lemmas:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3))) → *10_3, rt ∈ Ω(n11₃)

Generator Equations:
gen_cons:nil8_3(0) ⇔ nil
gen_cons:nil8_3(+(x, 1)) ⇔ cons(p(hole_a6_3), gen_cons:nil8_3(x))
gen_if:x'2d:x'2b:iff:x'2a:p9_3(0) ⇔ p(hole_a6_3)
gen_if:x'2d:x'2b:iff:x'2a:p9_3(+(x, 1)) ⇔ if(p(hole_a6_3), gen_if:x'2d:x'2b:iff:x'2a:p9_3(x))

No more defined symbols left to analyse.

(15) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3))) → *10_3, rt ∈ Ω(n11₃)

(16) BOUNDS(n^1, INF)